\begin{tabbing}
es{-}frame(${\it es}$;$i$;$L$;$x$;$T$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=es{-}dtype(${\it es}$; $i$; $x$; $T$)\+
\\[0ex]c$\wedge$ alle{-}at(\=${\it es}$;\+
\\[0ex]$i$;
\\[0ex]$e$.(($\neg$(es{-}kind(${\it es}$; $e$) $\in$ $L$ $\in$ Knd))
\\[0ex]$\Rightarrow$ (es{-}after(${\it es}$; $x$; $e$) = es{-}when(${\it es}$; $x$; $e$) $\in$ $T$)))
\-\-
\end{tabbing}